*Update*: 10 benchmark cases have been released in the Testcase session.
*Update*: 4 benchmark cases have been released in the Testcase session.
Efficiently solving the combinational single-output netlist is an important core engine, which is widely and frequently used for conquering the modern front-end problems, such as logic rewriting, false path analysis, property checking, and equivalence checking. In practical usage, one application would solve numerous sub-problems where each sub-problem is formulated in a single-output netlist. Although the sub-problems may be varied in their structure and topology, they have similar circuit characteristics like: size, depth, and combinations. Although we cannot directly reuse the learnt data, we can rely on the learnt characteristic to optimize the solving process among the numerous sub-problems for reducing the total runtime. Besides, the runtime for solving a single-output function is decided by two factors: the CNF encoding [1-4,11] and the SAT solving [5]. If we can explore the best CNF encoding setting and the best SAT solver setting by the small set of sampled sub-problems, we can significantly reduce the total runtime for solving the numerous similar sub-problems. In this contest, we request the participant to write a program that explores the best setting of the CNF encoder and the SAT solver.
State-of-the-art SAT solvers [6] have smart decision and learning procedures [7-9] for dealing with the various applications by the set of global optimized parameters. However, these parameters are not the best for solving a particular SAT instance. Fortunately, in our practical experience, if the parameters are useful for one case, they would also be useful for cases with similar characteristics. This means, if we can explore the best setting, we can use it to guide the solver amongst the SAT instances in a problem or amongst the problems with the similar characteristics. In addition to the SAT solver setting, the CNF encoding for a netlist is an important factor that affects the solving process. Therefore, the good encoding and solver setting can guide the solving and significantly reduce the total runtime for solving all the sub-problems. Therefore, the industrial approach to using the SAT solver would have two phases: the setting exploration phase—to decide the best encoder and solver setting, and the solving phase—to solve numerous similar problems, based on the generated encoder and solver setting. In this contest, in the setting exploration phase, we ask the participant to optimize the CNF encoding setting and the SAT solver setting simultaneously from the sampled sub-problems, called samples. In the solving phase, we will evaluate the quality of optimized settings on the remaining sub-problems, called tests. Therefore, the requested program should have two modes: in setting exploration phase, your program should optimize and generate the SAT solver setting and encoder setting based on the small set of samples, and in the solving phase, your program becomes a CNF encoder that converts a test into a CNF, based on your optimized setting. Furthermore, we will evaluate the solving runtime based on the solver setting and the generated CNF. The one that correctly solves the most tests within the shortest runtime will be recognized the best tool and win the contest.Figure 1. flow chart of the program requirement
Figure.1 shows the flow chart of the program requirements and the solving process for a case. Each case contains three samples and ten tests, where the sample and the test are the single-output combinational gate-level netlist in Verilog format. There are two phases for each case: the setting exploration phase and the solving phase for 10 tests (i.e. 1 time exploration, 10 times solving). In the exploration phase, your program should be in exploration mode. In the solving phase, your program is in generation mode and becomes a CNF encoder optimized by the encoder setting. Your program should be named ”expcnf” with two modes named ”-exp” for the exploration mode and ”-gen” for the generation mode. We explain the detailed description in the following paragraphs.
Notes: 10 testsare far from the real problem, but to ease evaluation we have limited it to just 10 tests for each case.In the setting exploration phase, the requested program is in exploration mode and accepts three samples and generates the solver setting and encoder setting within 1800 seconds. The program execution would be:
expcnf –exp <sample1.v> <sample2.v> <sample3.v> <EncoderSetting> <SATSolverSetting> |
The encoder setting should be in a single file and can be any format that you define and contain any information you learned in the exploration phase. The SAT solver setting is a single line command in a file that specifies one solver with its arguments, like “solver_a -ccmin-mode=1” where solver_a is the chosen solver and -ccmin-mode=1 is the used argument.
The participant can only use one of the following solvers:
Lingeling ats (in name lingeling)
http://fmv.jku.at/lingeling/lingeling-ats-57807c8-131016.tar.gz
Glucose 3.0 (in name glucose)
http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-3.0.tgz
Minisat 2.2 (in name minisat)
To be fair, we installed the listed solvers onto our evaluation machine and will base the evaluation on our compiled solvers. The input of our program is 3 samples. A sample must be in Verilog format and contains flattened, combinational gate-level netlist composed of only primitive gate.
Note: The solver here should contain only the executable binary name without the path.
In each solving phase, the requested program is in generation mode and accepts the generated encoder setting file to convert a test into a satisfiable equivalence CNF file. The program execution would be:
expcnf –gen <EncoderSetting> <test.v> <CNF output> |
The satisfiable equivalence CNF means:
The generated CNF is satisfiable if and only if the output of given netlist could be one.
The format of a test is the same as the sample in exploration mode, it is in Verilog format and contains flattened, combinational gate-level netlist composed of only primitive gate. The CNF file format is in DIMACS CNF format [10].
There are 10 tests in a case, in solving phase. For each case, it would generate 10 CNF files. We will solve each CNF file using the solver setting you generated in the exploration phase. For each test, the runtime of CNF generation is t_{1} and the runtime of SAT solving is t_{2}. We calculate the cost using the function 4 × t_{1} + t_{2}. We multiply 4 in runtime of CNF generation because we want the contest to focus on fast CNF generation. The program with the least total cost wins.
Language: C or C++
Compiler: GCC(G++) 3.4.6/4.4.7/4.8.0
Platform: Linux OS (CentOS 4.8), Intel Xeon E5420 @ 2.5GHz, 48 GB RAM (to be finalized)
We will select 2 open cases and 10 hidden cases for evaluation. Each case contains 3 samples for the exploration phase and 10 tests for the solving phase. Each case will have a cost value evaluated by the following process.
Exploration phase:The time limit for exploration phase is 1800 seconds. If it exceeds this time, we will not enter the solving phase and the cost for this case will be 3000. Otherwise, the cost is determined by the solving phase.
Solving phase:
The results (SAT or UNSAT) return by the SAT engine should be correct. Otherwise, you will be disqualified.
You will get a cost for each test according to the runtime of CNF generation ( t_{1} seconds) and the runtime for solving the CNF (t_{2} seconds). The cost is 4 × t_{1} + t_{2} only when t_{1} < 25 s and t_{2} < 100 s. Otherwise, the cost will be 300. The summation cost of 10 tests is the cost for this case.
If the results of all cases are correct, the summation cost of 12 cases is the total cost of your program. The program with least total cost wins.
Niklas Eén, Alan Mishchenko, and Niklas Sörensson, "Applying Logic Synthesis for Speeding Up SAT", SAT 2007.
Benjamin Chambers, Panagiotis Manolios, "Faster SAT Solving with Better CNF Generation", DATE 2009.
Niklas Eén, Armin Biere, "Effective Preprocessing in SAT through Variable and Clause Elimination", SAT 2005.
Marijn Heule, Matti Jarvisalo,and Armin Biere, "Clause Elimination Procedures for CNF Formulas", LPAR-17, 2010.
Joao P. Marques Silva, Karem A. Sakallah, "GRASP-A New Search Algorithm for Satisfiability", ICCAD 1996.
Niklas Eén, Niklas Sörensson, "An Extensible SAT-solver", SAT 2003.
Matthew W. Moskewicz, C.F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, "Chaff: Engineering an Efficient SAT Solver", DAC 2001.
Jinbo Huang, "The Effect of Restarts on the Efficiency of Clause Learning", IJCAI 2007.
Gilles Audemard, Laurent Simon, "Predicting Learnt Clauses Quality in Modern SAT Solvers", IJCAI 2009.
DIMACS CNF format http://logic.pdmi.ras.ru/~basolver/dimacs.html
M.N. Velev, Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors, Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004, pp. 310-315.
Are there any further information about the relation between sample and test designs?
Would you mind list all types of gate belonging to primitive gates? And what is the maximum input pin number of the gates?
Which solver is used for solving optimized CNF file after solving phase? Could participant choose ideal solver for their encoding?
At the third paragraph 'Example' solving phase. Is Input :verilog netlist mapping correctly to Output:CNF file?
May I know whether multi-threading is allowed for the problem "Simultaneous CNF Encoder Optimization with SAT solver Setting Selection"? And, do we have to submit our source code? We would also like to know whether the system can execute binaries compiled in newer linux version (say the version of g++ is 4.6.3).
The link provided on the problem description website for minisat, http://minisat.se/downloads/minisat-2.2.0.tar.gz, appears to be a dead link. Actually, as far as I can tell, the entire minisat.se domain is down, and has been for at least the last three weeks. I have tried installing directly from Niklas Sörensson's github repository for the minisat project, but I'm receiving a weird dynamically linked library issue that I think is probably explained on the website :). Do you know anything about the website being down, and if it will return?
Due to the number of output file is exactly one as the problem description, could we delete the others during the exploration and solving phase?
Is there any contraints on the number of executable file "expcnf"? Could the problem be performed as problem description using multiple executable files?
Since the linux system in the evaluation environment is pretty old, we are afraid that our program cannot be executed in that environment because of kernel incompatibility. Could you please advice on whether it is safe to use execvp() to execute the solvers installed in the system? Do we have to submit our source code?
Is it possible to release the SAT/UNSAT results of all utx cases? The SAT-solvers take so much time solving the problems for obtaining the golden results for verification.
That was a question in Q&A mention that this contest can't use multi-threading for fairness. and i was use tool ABC berkeley(using multi-threading) and submit in alpha test then get grade, so is that really OK to use ABC in this contest?
Does the evaluation and time out condition based on CPU time?
We find that in the beta submission we used the word "lingeline" to run the program and it works. However, the website say that the name should be "lingeling". We want to make sure that if both names can work. Or we should use "lingeling" to run our program?
Why the costs on the website of ut2 in the alpha submission are better than that of the beta submission? Do they run in different work station?
We'd like to use some tools during our CNF generation. Are we allowed to submit some perl files / executable files and call them within our main code during the generation phase?
Cases | Best result | 2nd result | 3rd result |
cost of ut1 | 147.28 | 1315.6 | 1381.77 |
cost of ut2 | 637.28 | 758.06 | 799.18 |
Cases | Best result | 2nd result | 3rd result |
cost of ut1 | 55.7 | 521.67 | 552.15 |
cost of ut2 | 1070.25 | 1146.62 | 1156.39 |
cost of ut3 | 3000 | 3000 | 3000 |
cost of ut5 | 1643.63 | 1902.32 | 1906.79 |
cost of ut7 | 97.53 | 734.45 | 853.41 |
cost of ut8 | 228.58 | 1956.21 | 1973.68 |
cost of ut13 | 999.68 | 1542.88 | 1646.52 |
cost of ut14 | 3000 | 3000 | 3000 |
cost of ut15 | 2710.12 | 2765.44 | 3000 |
cost of ut20 | 2701.84 | 2705.72 | 2708.88 |
cost of ut26 | 3000 | 3000 | 3000 |
cost of ut32 | 1935.5 | 1974.21 | 2023.78 |
cost of ut36 | 2395.95 | 2401.03 | 2401.26 |
cost of ut41 | 3000 | 3000 | 3000 |